<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2019</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
\usepackage{agda}

\begin{document}

</a><a id="62" class="Markup">\begin{code}</a>
<a id="75" class="Comment">-- We use non-standard spaces between the name of the term and the</a>
<a id="142" class="Comment">-- colon.</a>
<a id="152" class="Keyword">postulate</a>
  <a id="s00A0"></a><a id="164" href="Issue2019.html#164" class="Postulate">s00A0</a> <a id="170" class="Symbol">:</a> <a id="172" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="177" class="Comment">-- NO-BREAK SPACE        (&quot;\ &quot; with Agda input method)</a>
  <a id="s2004"></a><a id="234" href="Issue2019.html#234" class="Postulate">s2004</a> <a id="240" class="Symbol">:</a> <a id="242" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="247" class="Comment">-- THREE-PER-EM SPACE    (&quot;\;&quot; with Agda input method)</a>
  <a id="s202F"></a><a id="304" href="Issue2019.html#304" class="Postulate">s202F</a> <a id="310" class="Symbol">:</a> <a id="312" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="317" class="Comment">-- NARROW NO-BREAK SPACE (&quot;\,&quot; with Agda input method)</a>
<a id="372" class="Markup">\end{code}</a><a id="382" class="Background">

% Various whitespace characters: &quot;    &quot;.
</a><a id="425" class="Markup">\begin{code}</a>
<a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Agda.Builtin.String.html" class="Module">Agda.Builtin.String</a>

<a id="471" class="Comment">-- Various whitespace characters: &quot;    &quot;.</a>

<a id="various-whitespace-characters"></a><a id="514" href="Issue2019.html#514" class="Function">various-whitespace-characters</a> <a id="544" class="Symbol">:</a> <a id="546" href="Agda.Builtin.String.html#309" class="Postulate">String</a>
<a id="553" href="Issue2019.html#514" class="Function">various-whitespace-characters</a> <a id="583" class="Symbol">=</a> <a id="585" class="String">&quot;    &quot;</a>
<a id="592" class="Markup">\end{code}</a><a id="602" class="Background">

\end{document}
</a></pre></body></html>